T, T':Type, a:(T List), x:T', f:({x:T| (x  a)} T').
(x  map(f;a))  (y:T. ((y  a) & x = f(y))) 

latex

Definitions	(x  l), {x:A| B(x)} , x:AB(x), x:A. B(x), type List, Type, s = t, x:A  B(x), P & Q, x:A. B(x), P  Q, P  Q, P  Q, a < b, t  T, f(a), , A c B, x.A(x), x. t(x), map(f;as)
Lemmas	l member-set, map wf, l member subtype, subtype rel set, l member wf, member map, list-set-type